Nuprl Lemma : conditional-idempotent
11,40
postcript
pdf
T
,
V
:Type,
A
:(
T
),
dcd_A
:(
t
:
T
Dec(
A
(
t
))),
g
:(
T
V
). [
A
?
g
:
g
] =
g
latex
Definitions
Type
,
t
T
,
,
x
:
A
B
(
x
)
,
f
(
a
)
,
x
:
A
.
B
(
x
)
,
Dec(
P
)
,
[
P
?
f
:
g
]
,
<
a
,
b
>
,
s
=
t
,
left
+
right
,
P
Q
,
P
Q
,
if
p
:
P
then
A
(
p
) else
B
fi
Lemmas
decidable
wf
origin
T, V:Type, A:(T
), dcd_A:(t:TDec(A(t))), g:(TV). [A? g : g] = g T, V:Type, A:(T), dcd_A:(t:TDec(A(t))), g:(TV). [A? g : g] = g 
TB(x)x:A. B(x)
Q
Q